Electronic circuits, such as integrated microcircuits, are used in a variety of products, from automobiles to microwaves to personal computers. Designing and fabricating microcircuit devices typically involves many steps, sometimes referred to as the “design flow.” The particular steps of a design flow often are dependent upon the type of microcircuit, its complexity, the design team, and the microcircuit fabricator or foundry that will manufacture the microcircuit. Typically, software and hardware “tools” verify the design at various stages of the design flow by running software simulators and/or hardware emulators. These steps aid in the discovery of errors in the design, and allow the designers and engineers to correct or otherwise improve the design. These various microcircuits are often referred to as integrated circuits (IC's).
Several steps are common to most design flows. Initially, the specification for a new circuit is transformed into a logical design, sometimes referred to as a register transfer level (RTL) description of the circuit. With this logical design, the circuit is described in terms of both the exchange of signals between hardware registers and the logical operations that are performed on those signals. The logical design typically employs a Hardware Design Language (HDL), such as the Very high speed integrated circuit Hardware Design Language (VHDL). The logic of the circuit is then analyzed, to confirm that it will accurately perform the functions desired for the circuit, i.e. that the logical design conforms to the specification. This analysis is sometimes referred to as “formal verification.”
After the logical design is verified, it is converted into a device design by synthesis software. The device design, which is typically in the form of a schematic or netlist, describes the specific electronic devices (such as transistors, resistors, and capacitors) that will be used in the circuit, along with their interconnections. This device design generally corresponds to the level of representation displayed in conventional circuit diagrams. The relationships between the electronic devices are then analyzed, often mathematically, to confirm that the circuit described by the device design conforms to the logical design, and as a result, the specification. This analysis is also sometimes referred to as formal verification. Additional verifications, such as for example timing and power verifications are often made at this stage, and may be included in the formal verification process.
Once the components and their interconnections are established, the design is again transformed, this time into a physical design that describes specific geometric elements. The geometric elements, which typically are polygons, define the shapes that will be created in various layers of material to manufacture the circuit. This type of design often is referred to as a “layout” design. The layout design is then used as a template to manufacture the integrated circuit. More particularly, the integrated circuit devices are manufactured, by for example an optical lithographic process, using the layout design as a template. During an optical lithography process, a photo-mask is used to transfer a geometric pattern from the photo-mask onto a substrate via a photo-resistive material. The geometric pattern in the photo-mask is designed such that the image or pattern transferred onto the substrate matches the geometric pattern of the layout design.
As indicated above, formal verification is used to ensure the design complies with the specification. The specification often defines properties and directives that collectively describe the expected behavior of the device. The specification of properties and directives is often done semantically. Various languages exist for defining properties and directives, such as for example Sugar, ForSpec, Property Specification Language (PSL), and System Verilog Assertions (SVA), among others. As stated above, the device design is often in the form of a hardware description language. Formal verification then either proves or disproves the properties and directives with respect to the design and the specification.
As modern device designs and specification are extremely complicated, computing devices, executing a formal verification toolset are often employed. These formal verification tools typically report out to the user which properties are proven true, and what properties can fail as well as what sequences of states in the design can cause the properties to fail.
As stated, modern designs are increasingly complex. Part of this complexity is manifest in low power designs, where different power supplies are used for differing parts of the design. For example, many modern electronic devices are capable of performing a multitude of functions. For example, a cell phone may include a camera in addition to the other components needed to transmit and receive voice communications. During times that the camera is not in use it may be desirable to turn off power to the image capture portions of the device, so as not to prematurely drain the battery or use excessive power. As a result, the device would need multiple power supplies or power switches capable of delivering power to one portion of the device while shutting of power delivery to another portion of the device. Often when a portion of a device is supplied power by a particular power supply, it is said that the portion of the device is “driven” by that particular power supply.
Portions of a device being “driven” by different power supplies are said to be in different power domains. Accordingly, the image capture portions of the design above would be in a different power domain than other portions of the design. Power domains, as well as other low power design techniques are further described in Low Power Methodology Manual For System-On-Chip Design, by M. Keating et al., Springer 2007, which book is incorporated entirely herein by reference.
Various standards exist for the specification of low power design features. For example, the Unified Power Format (UPF) and the Common Power Format (CPF) are two such standards. Designs with multiple power supplies, and low power designs in particular have a functional specification and a power specification. The functional specification defines the behavior of the device while the power specification defines the power domains and power controller information. For low power designs, the basic functionality of the design as well as the low power features must be verified. The verification considers how the power supply network is created, how power supply nets behave as well as ensures that various scenarios of powering up and powering down different power domains do not interfere with the intended functionality of the design.
Various approaches to verifying low power designs are discussed in Assertion-Based Verification For Power Cycled Systems-On-Chip, by T. Anderson et al., Design and Verification Conference and Exhibition Proceedings, San Jose, Calif., Feb. 19-21, 2008, To Retain Or Not To Retain: How Do I Verify The State Elements Of My Low Power Design?, by S. Baily et al., Design and Verification Conference and Exhibition Proceedings, San Jose, Calif., Feb. 19-21, 2008, Upping Verification Productivity Of Low Power Designs, by G. Chidolue et al., Design and Verification Conference and Exhibition Proceedings, San Jose, Calif., Feb. 19-21, 2008, Power Assertions And Coverage For Improving Quality Of Low Power Verification Closure Of Power Intent, by N. Khan et al., Design and Verification Conference and Exhibition Proceedings, San Jose, Calif., Feb. 19-21, 2008, and Static And Formal Verification Of Power Aware Designs At The RTL Using UPF, by R. Mukherjee et al., Design and Verification Conference and Exhibition Proceedings, San Jose, Calif., Feb. 19-21, 2008, which articles are all incorporated entirely herein by reference.
The various approaches to verifying low power designs mentioned above all require modification to the functional specification. For example, the properties defined by the functional specification may be altered to explicitly state the power state information. However, this approach clutters the functional specification and particularly the properties. Additionally, this approach requires additional time and energy from the designer to modify the functional specification according to the power specification.